%% LyX 2.3.6.1 created this file.  For more info, see http://www.lyx.org/.
%% Do not edit unless you really know what you are doing.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%teste
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\documentclass[brazil,oldfontcommands]{memoir}
\usepackage{lmodern}
\usepackage{lmodern}
\usepackage[T1]{fontenc}
\usepackage[latin9]{inputenc}
\usepackage{xcolor}
\definecolor{page_backgroundcolor}{rgb}{1, 1, 1}
\pagecolor{page_backgroundcolor}
\definecolor{document_fontcolor}{rgb}{0, 0, 0}
\color{document_fontcolor}
\usepackage{babel}
\usepackage{array}
\usepackage{prettyref}
\usepackage{calc}
\usepackage{mathrsfs}
\usepackage{amsmath}
\usepackage{amsthm}
\usepackage{amssymb}
\OnehalfSpacing
\usepackage[unicode=true,
 bookmarks=false,
 breaklinks=true,pdfborder={0 0 0},pdfborderstyle={},backref=page,colorlinks=true]
 {hyperref}
\hypersetup{
 hidelinks,pdfcreator={LaTeX via pandoc}}

\makeatletter

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% LyX specific LaTeX commands.
%% Because html converters don't know tabularnewline
\providecommand{\tabularnewline}{\\}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Textclass specific LaTeX commands.
\theoremstyle{plain}
\ifx\thechapter\undefined
	\newtheorem{thm}{\protect\theoremname}
\else
	\newtheorem{thm}{\protect\theoremname}[chapter]
\fi
\theoremstyle{definition}
\newtheorem{defn}[thm]{\protect\definitionname}
\theoremstyle{definition}
\newtheorem{example}[thm]{\protect\examplename}
\theoremstyle{plain}
\newtheorem{prop}[thm]{\protect\propositionname}
\theoremstyle{plain}
\newtheorem{lem}[thm]{\protect\lemmaname}

\@ifundefined{date}{}{\date{}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% User specified LaTeX commands.
\usepackage{pxfonts}
\usepackage{tikz}
\usepackage[usenames,dvipsnames]{pstricks}
\usepackage{epsfig}
\usepackage{pst-grad} % For gradients
\usepackage{pst-plot} % For axes
\usepackage[space]{grffile} % For spaces in paths
\usepackage{etoolbox} % For spaces in paths
\makeatletter % For spaces in paths
\patchcmd\Gread@eps{\@inputcheck#1 }{\@inputcheck"#1"\relax}{}{}
\makeatother
\newtheorem*{problem*}{\protect\problemname}
\providecommand{\problemname}{Problema}
\usepackage[dvipsnames]{xcolor} 	% para cores
\makeatletter
\hypersetup{
     	%pagebackref=true,
pdftitle={\@title}, 
pdfauthor={\@author},
  %  	pdfsubject={\imprimirpreambulo},
    pdfcreator={LaTeX with abnTeX2},
pdfkeywords={abnt}{latex}{abntex}{abntex2}{livro}, 
colorlinks=true,       		% false: boxed links; true: colored links
    	linkcolor=blue,          	% color of internal links
    	citecolor=blue,        		% color of links to bibliography
    	filecolor=magenta,      		% color of file links
urlcolor=blue,
bookmarksdepth=4
}
\makeatother

\makeatother

\providecommand{\definitionname}{Definição}
\providecommand{\examplename}{Exemplo}
\providecommand{\lemmaname}{Lema}
\providecommand{\propositionname}{Proposição}
\providecommand{\theoremname}{Teorema}

\begin{document}
\title{Caixas e diamantes: uma introdução aberta à lógica modal}
\author{Remixado por Richard Zach}

\maketitle
\frontmatter

\tableofcontents*

\chapter{Prefácio}

\chapter{Introdução}

Lógicas modais são extensões da lógica clássica por meio da introdução
dos operadores $\square$ (``caixa'') e $\diamondsuit$ (``diamante''),
que se anexam a fórmulas. Intuitivamente, $\square$ pode ser lido
como ``necessariamente'' e $\diamondsuit,$como ``possivelmente.
Assim $\square p$ é ``$p$ é necessariamente verdadeira'' e $\diamondsuit p$
é ``$p$ é possivelmente verdadeira''. Uma vez que necessidade e
possibilidade são noções metafísicas fundamentais, lógica modal é,
obviamente, de grande interesse filosófico. Ela permite a formalização
de princípios metafísicos tais como ``$\square p\rightarrow p$''
(se $p$ é necessária, então ela é verdadeira) ou ``$\diamondsuit p\rightarrow\square\diamondsuit p$''
(se $p$ é possível, ela é necessariamente possível).

Os operadores $\square$ e $\diamondsuit$ são \emph{intensionais}.
Isto significa que a verdade ou falsidade de $\square A$ ou $\diamondsuit A$
não dependem apenas da verdade ou falsidade de $A$. Um operador que
não é intensional é extensional. A negação é extensional: $\neg A$
é verdadeiro se e somente (sse) $A$ é falso; assim, o valor de verdade
de $\neg A$ depende somente do valor de verdade de $A$. $\square$
e $\diamondsuit$ não são dessa forma. O valor de verdade de $\square A$
ou de $\diamondsuit A$ depende também do significado de $A$. Embora
a semântica verofuncional seja suficiente para lidar com operadores
extensionais, operadores intensionais como $\square$ e $\diamondsuit$
requerem um tipo diferente de semântica. Uma dessas semânticas que
toma um lugar central neste livro é a semântica relacional (também
chamada semântica de mundos possíveis ou semântica de Kripke).

A lógica que corresponde à interpretação de $\square$ como ``necessariamente''
tem uma semântica que é é relativamente simples: em vez de atribuir
valores de verdade às variáveis proposicionais, uma interpretação
$\mathbf{M}$ atribui a um conjunto de ``mundos'' a elas --- intuitivamente,
aqueles mundos em que $p$ é interpretado como verdadeiro. Com base
em uma tal interpretação, podemos definir uma relação de satisfação.
A definição desta relação de satisfação torna $\square A$ satisfeita
em um mundo $w$ sse $A$ é satisfeita em \emph{todos} os mundos:
$\mathbf{M},w\Vdash\square A$ sse $\mathbf{M},v\Vdash A$, para todos
os mundos $v$. Isto corresponde à ideia de Leibniz segundo a qual
o que é necessariamente verdadeiro é o que é verdadeiro em qualquer
mundo possível.

``Necessariamente'' não é a única maneira de se interpretar o operador
$\square$, mas é a padrão --- ``necessariamente'' e ``possivelmente''
são as então chamadas modalidades \emph{aléticas}. Em outras interpretações,
$\square$ é lido como ``é conhecido (por alguma pessoa \emph{A})
que'', como ``alguma pessoa \emph{A} acredita que'', como ``deveria
ser o caso que'' ou como ``sempre será verdadeiro que''. Estas
são, respectivamente, modalidades epistêmicas, doxásticas, deônticas
e temporais. Interpretações diferentes de $\square$ farão com que
uma mesma fórmula seja logicamente verdadeira em uma interpretação
e não logicamente verdadeira em outra; da mesma forma, uma certa inferência
pode ser válida em uma interpretação e inválida na outra. Por exemplo,
tudo que é necessário é verdadeiro ou tudo que é conhecido é verdadeiro,
assim $\square A\rightarrow A$ é uma verdade lógica nas interpretações
alética e epistêmica. Por outro lado, nem tudo que é acredito ou nem
tudo que deveria ser o caso é, de fato, o caso. Dessa forma, $\square A\rightarrow A$
não é uma verdade nas interpretações doxástica ou deôntica.

A fim de lidar com diferentes interpretações dos operadores modais,
a semântica é estendida por meio de uma relação entre mundos, a então
chamada relação de acessibilidade. Então $\mathbf{M},w\Vdash\square A$
sse $\mathbf{M},v\Vdash A$ para todos os mundos $v$ que são acessíveis
a partir de $w$. A semântica resultante é bastante versátil e poderosa,
e a ideia básica pode ser usada para fornecer interpretações semânticas
para lógicas baseadas em outros operadores intensionais. Uma dessas
lógicas é a lógica intuicionista, uma lógica construtiva baseada no
ramo da matemática construtiva de L. E. J. Brouwer. Lógica intuicionista
é filosoficamente interessante por esta razão --- ela desempenha
um papel importante na explicação construtiva da matemática {[}in
constructive accounts of mathematics{]}. Michael Dummett, influente
filósofo inglês do século 20, propôs a lógica intuicionista como uma
lógica superior à lógica clássica. Uma outra aplicação dos modelos
relacionais é quando eles são usados como semântica para condicionais
subjuntivos ou contrafactuais, uma abordagem que foi desbravada por
Robert Stalnaker e David K. Lewis.

Este livro é uma introdução à sintaxe, à semântica e à teoria da prova
de lógicas intensionais. Ela trata apenas de lógicas proposicionais,
embora edições futuras também lidarão com lógicas de predicados. O
material é dividido em três partes: a primeira parte lida com lógicas
modais normais. Estas são lógicas com os operadores $\square$ e $\diamondsuit$.
Discutimos a sintaxe delas, modelos relacionais e noções semânticas
baseadas nesses modelos (tais como validade e consequência) e sistemas
de provas (tanto sistemas axiomáticos como tablôs). Estabelecemos
alguns resultados sobre estas lógicas tais como correção e completude
dos sistemas de provas considerados e discutimos algumas construções
modelo-teóricos {[}model-theoretic construction{]} tais como filtrações.
A segunda parte trada da lógica intuicionista. Aqui discutimos dedução
natural e derivações axiomáticas, semânticas relacionais e topológica
e correção e completude dos sistemas de provas. A terceira parte lida
com a semântica Lewis-Stalnaker dos condicionais contrafactuais. O
apêndice discute algumas ideias e resultados da teoria de conjuntos
e da teoria das relações que são cruciais para a semântica relacional
assim como recapitula a sintaxe, semântica e teoria da prova da lógica
proposicional clássica.

\mainmatter

\part{Lógicas modais normais}

\chapter{Sintaxe e semântica das lógicas normais modais}

\section{Introdução}

Lógica modal lida com proposições \emph{modais} e com as relações
de acarretamento {[}entailment{]} que ocorre entre elas. Exemplos
de proposições modais são os seguintes:
\begin{enumerate}
\item É necessário que $2+2=4$
\item É necessariamente possível que chova amanhã
\item Se é necessariamente possível que $A$, então é possível que $A$
\end{enumerate}
Possibilidade e necessidade não são as únicas modalidades: outros
conectivos unários são também classificados como modalidades, por
exemplo, ``deveria ser o caso que $A$'', ``Dana sabe que $A$''
ou ``Dana acredita que $A$''.

A primeira aparição da lógica modal ocorre no livro \emph{Da Interpretação}
de Aristóteles: ele foi o primeiro a perceber que necessidade implica
possibilidade, mas não vice-versa; que possibilidade e necessidade
são interdefiníveis; que se $A\wedge B$ é possivelmente verdadeira,
então $A$ é possivelmente verdadeira e $B$ é possivelmente verdadeira,
mas não inversamente; e que se $A\rightarrow B$ é necessária, então
se $A$ é necessária, então $B$ é necessária.

A primeira abordagem moderna da lógica modal foi o trabalho de C.
I. Lewis, que culminou no livro \emph{Lógica Simbólica} (1932) de
Lewis e Langford. Lewis e Langford estavam insatisfeitos com a representação
da implicação por meio do condicional material: $A\rightarrow B$
é um substituto pobre para ``A implica B''. Em vez disso, eles propuseram
caracterizar implicação como ``Necessariamente, se $A$, então $B$'',
simbolizada como $A\strictif B$. Tentando isolar diferentes propriedades,
Lewis identificou cinco sistema modais diferentes, \textbf{S1}, \textbf{S2},
\textbf{S3}, \textbf{S4}, \textbf{S5}, sendo as duas últimas ainda
usadas.

A abordagem de Lewis e Langford foi puramente sintática: eles identificaram
axiomas e regras razoáveis e investigaram o que era derivável por
esses meios. Uma abordagem semântica continuou indescritível por muito
tempo {[}A semantic approach remained elusive for a long time{]},
até que uma primeira tentativa foi feita por Rudolf Carnap em \emph{Significado
e Necessidade} (1947) usando a noção de \emph{descrição de estado},
isto é, uma coleção de sentenças atômicas (aquelas que são ``verdadeiras''
neste estado de descrição). Depois de apresentar a definição de verdade
para sentenças arbitrárias $A$ {[}After lifting the truth definition
to arbitrary sentences A{]}, Carnap define A como sendo \emph{necessariamente
verdadeira}, se ela é verdadeira em todas as descrições de estado.
A abordagem de Carnap não poderia lidar com modalidades \emph{iteradas},
já que sentenças da forma ``Possivelmente é necessário que $A$ é
possível'' sempre se reduzem à modalidade mais interna {[}innermost{]}.

O maior avanço {[}breakthrough{]} na semântica modal veio com artigo
``Um teorema da completude na lógica modal'' (JSL 1959) de Saul
Kripke. Kripke baseou o seu trabalho na ideia de Leibniz segundo a
qual um enunciado é necessariamente verdadeiro se ele é verdadeiro
``em todos os mundos possíveis''. Esta ideia , entretanto, sofre
das mesmas desvantagens {[}drawbacks{]} que a de Carnap, já que a
verdade do enunciado em um mundo $w$ (ou em uma descrição de estado
$s$) não depende de $w$ absolutamente. Assim Kripke assumiu que
os mundos estão relacionados por meio de uma \emph{relação de acessibilidade}
$R$ e que um enunciado da forma ``Necessariamente $A$'' é verdadeira
em um mundo $w$ se e somente se $A$ é verdadeiro em todos os mundos
$w'$ acessíveis a partir de $w$. Semânticas que ofereceram alguma
versão desta abordagem são chamadas semênticas de Kripke e possibilitaram
o desenvolvimento turbulento {[}tumultuous development{]} das lógicas
modais (no plural).

Quando interpretada pelas semânticas de Kripke, lógica modal mostra-nos
como são as estruturas relacionais ``de dentro''. Uma estrutura
relacional é exatamente um conjunto abastecido com uma relação binária
(por exemplo, o conjunto de estudantes na sala de aula ordenados pelo
numeração da carteira de identidade (ou cpf) é uma estrutura relacional).
Mas, de fato, estruturas relacionais estão disponíveis {[}come in{]}
em todos os tipos de domínios: além da possibilidade relativa dos
estados do mundo, podemos ter estados epistêmicos de algum agente
relacionado por possibilidade epistêmica ou ter estados de um sistema
dinâmico com as transições de estado deles, etc. Lógica modal pode
ser usada para modelar todos estes: a primeira estrutura nos dá lógica
modal ordinária, alética; as outras nos são lógica epistêmica, lógica
dinâmica, etc.

Focamos em um ângulo particular, conhecido pelos lógicos modais como
``teoria da correspondência''. Uma das mais significantes descobertas
iniciais de Kripke é que muitas propriedades da relação de acessibilidade
$R$ (se ela é transitiva, simétrica, etc) podem ser caracterizadas
\emph{na própria linguagem modal} por meio de ``esquemas modais''
apropriados. Lógicos modais dizem, por exemplo, que a reflexividade
de $R$ ``corresponde'' ao esquema ``Se necessariamente $A$, então
$A$''. Exploramos principalmente a teoria da correspondência de
alguns sistemas clássicos de lógica modal (por exemplo, \textbf{S4}
e \textbf{S5}) obtidos por meio da combinação dos esquemas D, T, B,
4 e 5.

\section{A linguagem da lógica modal básica\vspace{8pt}
}

\noindent{\fboxrule 0.1cm\fcolorbox{magenta}{white}{\begin{minipage}[t]{1\columnwidth - 2\fboxsep - 2\fboxrule}%
\begin{defn}
A linguagem básica da lógica modal contém
\end{defn}

\begin{enumerate}
\item A constante proposicional para falsidade $\bot$
\item Um conjunto infinito e enumerável de variáveis proposicionais: $p_{0},p_{1},p_{2},\ldots$
\item Os conectivos proposicionais: $\neg$ (negação), $\wedge$ (conjunção),
$\vee$ (disjunção), $\rightarrow$ (condicional)
\item O operador modal $\square$
\item O operador modal $\diamondsuit$
\end{enumerate}
%
\end{minipage}}}

\vspace{8pt}
\noindent{\fboxrule 0.1cm\fcolorbox{magenta}{white}{\begin{minipage}[t]{1\columnwidth - 2\fboxsep - 2\fboxrule}%
\begin{defn}
\emph{Fórmulas} da linguagem modal básica são indutivamente definidas
como se segue
\end{defn}

\begin{enumerate}
\item $\bot$ é uma fórmula atômica
\item Qualquer variável proposicional $p_{i}$ é uma fórmula (atômica)
\item Se $A$ e $B$ são fórmulas, então $(A\wedge B)$ é uma fórmula.
\item Se $A$ e $B$ são fórmulas, então $(A\vee B)$ é uma fórmula.
\item Se $A$ e $B$ são fórmulas, então $(A\rightarrow B)$ é uma fórmula.
\item Se $A$ é uma fórmula, então $\square A$ é uma fórmula
\item Se $A$ é uma fórmula, então $\diamondsuit A$ é uma fórmula
\item Nenhuma outra expressão é uma fórmula
\end{enumerate}
%
\end{minipage}}}\vspace{8pt}

\noindent{\fboxrule 0.1cm\fcolorbox{magenta}{white}{\begin{minipage}[t]{1\columnwidth - 2\fboxsep - 2\fboxrule}%
\begin{defn}
Fórmulas costruidas usando operadores definidos devem ser compreendidas
como se segue
\end{defn}

\begin{enumerate}
\item \ensuremath{\top} abrevia $\neg$$\bot$.
\item $A$\ensuremath{\leftrightarrow} $B$ abrevia $(A\rightarrow B)$
$\wedge$ $(B\rightarrow A)$.
\end{enumerate}
%
\end{minipage}}}

Se a fórmula $A$ não contém $\square$ ou $\diamondsuit$, dizemos
que ela é modalmente livre {[}modal-free{]}

\vspace{8pt}


\section{Substituição simultânea}

Uma instância de uma fórmula $A$ é o resultado da substituição de
todas as ocorrências de uma variável proposicional em $A$ por alguma
outra fórmula. Referir-nos-emos frequentemente às instâncias das fórmulas
tanto ao discutir validade com ao discutir derivabilidade. Portanto
é útil definir a noção precisamente.\vspace{8pt}

\noindent{\fboxrule 0.1cm\fcolorbox{magenta}{white}{\begin{minipage}[t]{1\columnwidth - 2\fboxsep - 2\fboxrule}%
\begin{defn}
Sejam $A$ uma fórmula modal em que todas as variáveis proposicionais
estão entre $p_{1},\ldots,p_{n}$ e $D_{1},\ldots,D_{n}$ fórmulas
também modais, definimos $A[D_{1}/p_{1},\ldots,D_{n}/p_{n}]$ como
o resultado de substituir simultaneamente cada um dos $p_{i}$ por
$D_{i}$ em $A$. Formalmente, isto é uma definição por indução sobre
{[}a complexidade de{]} $A$:
\end{defn}

\begin{enumerate}
\item $A\equiv\bot$: $A[D_{1}/p_{1},\dots,D_{n}/p_{n}]$ é $\bot$
\item $A\equiv q$: $A[D_{1}/p_{1},\dots,D_{n}/p_{n}]$ é $q$, dado que
$q\not\equiv p_{i}$ (para $i=1,\ldots,n$).
\item $A\equiv p_{i}$: $A[D_{1}/p_{1},\dots,D_{n}/p_{n}]$ é $D_{i}$
\item $A\equiv\neg B$: $A[D_{1}/p_{1},\dots,D_{n}/p_{n}]$ é $\neg B[D_{1}/p_{1},\dots,D_{n}/p_{n}]$
\item $A\equiv(B\wedge C)$: $A[D_{1}/p_{1},\dots,D_{n}/p_{n}]$ é $(B[D_{1}/p_{1},\dots,D_{n}/p_{n}]\wedge C[D_{1}/p_{1},\dots,D_{n}/p_{n}])$
\item $A\equiv(B\vee C)$: $A[D_{1}/p_{1},\dots,D_{n}/p_{n}]$ é $(B[D_{1}/p_{1},\dots,D_{n}/p_{n}]\vee C[D_{1}/p_{1},\dots,D_{n}/p_{n}])$
\item $A\equiv(B\rightarrow C)$: $A[D_{1}/p_{1},\dots,D_{n}/p_{n}]$ é
$(B[D_{1}/p_{1},\dots,D_{n}/p_{n}]\rightarrow C[D_{1}/p_{1},\dots,D_{n}/p_{n}])$
\item $A\equiv(B\leftrightarrow C)$: $A[D_{1}/p_{1},\dots,D_{n}/p_{n}]$
é $(B[D_{1}/p_{1},\dots,D_{n}/p_{n}]\leftrightarrow C[D_{1}/p_{1},\dots,D_{n}/p_{n}])$
\item $A\equiv\square B$: $A[D_{1}/p_{1},\dots,D_{n}/p_{n}]$ é $\square B[D_{1}/p_{1},\dots,D_{n}/p_{n}]$
\item $A\equiv\diamondsuit B$: $A[D_{1}/p_{1},\dots,D_{n}/p_{n}]$ é $\diamondsuit B[D_{1}/p_{1},\dots,D_{n}/p_{n}]$
\end{enumerate}
A fórmula $A[D_{1}/p_{1},\dots,D_{n}/p_{n}]$ é chamada uma instância
de substituição de $A$.%
\end{minipage}}}\vspace{8pt}

\begin{example}
Suponha que $A$ seja $p_{1}\rightarrow\square(p_{1}\wedge p_{2})$,
$D_{1}$, $\diamondsuit(p_{2}\rightarrow p_{3})$ e $D_{2}$, $\neg\square p_{1}$.
Então $A[D_{1}/p_{1},D_{2}/p_{2}]$ é $\diamondsuit(p_{2}\rightarrow p_{3})\rightarrow\square(\diamondsuit(p_{2}\rightarrow p_{3})\wedge\neg\square p_{1})$.
Por outro lado, $A[D_{2}/p_{1},D_{1}/p_{2}]$ é $\neg\square p_{1}\rightarrow\square(\neg\square p_{1}\wedge\diamondsuit(p_{2}\rightarrow p_{3}))$.
\end{example}

Note que substituição simultânea não é, em geral, o mesmo que substituição
iterada, por exemplo, compare $A[D_{1}/p_{1},D_{2}/p_{2}]$ acima
com $(A[D_{1}/p_{1}])[D_{2}/p_{2}]$ que é:
\begin{center}
$\diamondsuit(p_{2}\rightarrow p_{3})\rightarrow\square(\diamondsuit(p_{2}\rightarrow p_{3})\wedge p_{2})[\neg\square p_{1}/p_{2}]$,
ou seja,
\par\end{center}

\begin{center}
$\diamondsuit(\neg\square p_{1}\rightarrow p_{3})\rightarrow\square(\diamondsuit(\neg\square p_{1}\rightarrow p_{3})\wedge\neg\square p_{1})$.
\par\end{center}

\noindent E também compare com $(A[D_{2}/p_{2}])[D_{1}/p_{1}]$
\begin{center}
$p_{1}\rightarrow\square(p_{1}\wedge\neg\square p_{1})[\diamondsuit(p_{2}\rightarrow p_{3})/p_{1}]$,
ou seja,
\par\end{center}

\begin{center}
$\diamondsuit(p_{2}\rightarrow p_{3})\rightarrow\square(\diamondsuit(p_{2}\rightarrow p_{3})\wedge\neg\square\diamondsuit(p_{2}\rightarrow p_{3}))$.
\par\end{center}

\section{Modelos relacionais}

O conceito básico de semântica para lógicas modais normais é o de
\emph{modelo relacional}. O modelo consiste em um conjunto de mundos,
que estão relacionados por meio de uma ``\emph{relação de acessibilidade}''
binária, junto com uma atribuição que determina quais variáveis proposicionais
contam como ``verdadeiras'' nestes mundos.

\vspace{8pt}

\noindent{\fboxrule 0.1cm\fcolorbox{magenta}{white}{\begin{minipage}[t]{1\columnwidth - 2\fboxsep - 2\fboxrule}%
\begin{defn}
Um \emph{modelo} para linguagem modal básica é uma tripla ordenada
$\mathbf{M}=<W,R,V>$, em que
\end{defn}

\begin{enumerate}
\item $W$ é um conjunto não-vazio de ``mundos'';
\item $R$ é uma relação de acessibilidade binária sobre $W$ e;
\item $V$ é uma função que atribui a cada variável proposicional $p$ um
conjunto $V(p)$ de mundos possíveis.
\end{enumerate}
%
\end{minipage}}}

\vspace{8pt}
Quando $Rww'$ vale, dizemos que $w'$ \emph{é acessível a partir
de} $w$. Quando $w\in V(p)$, dizemos que $p$ \emph{é verdadeira
em }$w$.

A grande vantagem da semântica relacional é que modelos podem ser
representados por meio de diagramas simples, tais como o da Figura
\ref{fig:simples}. Mundos são representados por nódulos e o mundo
$w'$ é acessível a partir de $w$ exatamente quando há uma seta de
$w$ em direção a $w'$. Além disso, rotulamos um nódulo (mundo) por
$p$ quando $w\in V(p)$. Caso contrário, rotulamos o nódulo por $\neg p$.
A Figura \ref{fig:simples} representa o modelo com $W=\{w_{1},w_{2},w_{3}\},R=\{<w_{1},w_{2}>,<w_{1},w_{3}>\},V(p)=\{w_{1},w_{2}\}$
e $v(q)=\{w_{2}\}$.

\begin{figure}
\begin{centering}
\psscalebox{.7 .7} % Change this value to rescale the drawing. 
{ 
\begin{pspicture}(0,-3.9)(6.14,3.9) 
\pscircle[linecolor=black, linewidth=0.04, dimen=outer](0.88,-0.22){0.88} 
\pscircle[linecolor=black, linewidth=0.04, dimen=outer](4.64,3.02){0.88}
\pscircle[linecolor=black, linewidth=0.04, dimen=outer](4.62,-3.02){0.88}
\rput[bl](0.64,-0.32){$w_1$} \rput[bl](4.54,2.9){$w_2$} \rput[bl](4.38,-3.2){$w_3$} \rput[bl](2.04,-0.02){$p$} \rput[bl](1.94,-0.52){$\neg q$} \rput[bl](5.94,3.18){$p$}
\rput[bl](5.9,2.56){$q$} 
\rput[bl](5.74,-2.88){$\neg p$} 
\rput[bl](5.74,-3.42){$\neg q$}
\psline[linecolor=black, linewidth=0.04, arrowsize=0.05291667cm 2.0,arrowlength=1.4,arrowinset=0.0]{->}(1.64,-0.84)(3.6,-2.5) 
\psline[linecolor=black, linewidth=0.04, arrowsize=0.05291667cm 2.0,arrowlength=1.4,arrowinset=0.0]{->}(1.52,0.68)(3.66,2.44)
\end{pspicture} 
}
\par\end{centering}
\caption{Um modelo simples.\label{fig:simples}}
\end{figure}


\section{Verdade em um mundo}

Qualquer modelo modal determina quais fórmulas modais contam como
verdadeiras nos mundos dentro do modelo. A relação ``modelo $\mathbf{M}$
faz a fórmula $A$ verdadeira no mundo $w$'' é uma noção básica
de semântica relacional. A relação é definida indutivamente e coincide
com a caracterização habitual que usa tabelas de verdade para operadores
não-modais.\vspace{8pt}

\noindent{\fboxrule 0.1cm\fcolorbox{magenta}{white}{\begin{minipage}[t]{1\columnwidth - 2\fboxsep - 2\fboxrule}%
\begin{defn}
\emph{Verdade de uma fórmula A em} $w$ em um {[}modelo{]} $\mathbf{M}$
--- em símbolos: $\mathbf{M},w\Vdash A$ --- é definido por indução
da seguinte forma:
\end{defn}

\begin{enumerate}
\item $A\equiv\bot$: Nunca $\mathbf{M},w\Vdash\bot$;
\item $\mathbf{M},w\Vdash p$ sse $w\in V(p)$;
\item $A\equiv\neg B$: $\mathbf{M},w\Vdash A$ sse $\mathbf{M},w\nVdash B$;
\item $A\equiv(B\wedge C)$: $\mathbf{M},w\Vdash A$ sse $\mathbf{M},w\Vdash B$
e $\mathbf{M},w\Vdash C$;
\item $A\equiv(B\vee C)$: $\mathbf{M},w\Vdash A$ sse $\mathbf{M},w\Vdash B$
ou $\mathbf{M},w\Vdash C$;
\item $A\equiv(B\rightarrow C)$: $\mathbf{M},w\Vdash A$ sse $\mathbf{M},w\nVdash B$
ou $\mathbf{M},w\Vdash C$;
\item $A\equiv\square B$: $\mathbf{M},w\Vdash A$ sse $\mathbf{M},w'\Vdash B$
para todo $w'\in W$ com $Rww'$;
\item $A\equiv\diamondsuit B$: $\mathbf{M},w\Vdash A$ sse $\mathbf{M},w'\Vdash B$
para pelo menos um $w'\in W$ com $Rww'$;
\end{enumerate}
%
\end{minipage}}}\vspace{8pt}

Note que, de acordo com a cláusula 7, uma fórmula $\square B$ é verdadeira
em $w$, sempre que não há qualquer $w'$ tal que $Rww'$. Em um tal
caso, $\square B$ é vacuamente verdadeiro em $w$. $\square B$também
pode ser satisfeito em $w$, mesmo se $B$ não é. A verdade de $B$
em $w$ não garante a verdade de $\diamondsuit B$ em $w$. Isto vale,
entretanto, se $Rww$, ou seja, se $R$é reflexiva. Se não há $w'$
tal que $Rww'$, então $\mathbf{M},w\nVdash\diamondsuit A$, para
qualquer A.
\begin{prop}
1.$\mathbf{M},w\Vdash\square A$ sse $\mathbf{M},w\Vdash\neg\diamondsuit\neg A$

2. $\mathbf{M},w\Vdash\diamondsuit A$ sse $\mathbf{M},w\Vdash\neg\square\neg A$\label{proposicao1.7}
\end{prop}

\begin{proof}
1. $\mathbf{M},w\Vdash\neg\diamondsuit\neg A$ sse $\mathbf{M},w\nVdash\diamondsuit\neg A$por
meio da definição de $\mathbf{M},w\Vdash$. $\mathbf{M},w\Vdash\diamondsuit\neg A$
sse para algum $w'$ com $Rww'$, $\mathbf{M},w'\Vdash\neg A$. Logo,
$\mathbf{M},w\nVdash\diamondsuit\neg A$ sse para todo $w'$ com $Rww'$,
$\mathbf{M},w'\nVdash\neg A$. Também temos que $\mathbf{M},w'\nVdash\neg A$
sse $\mathbf{M},w'\Vdash A$. Juntando, temos que $\mathbf{M},w\Vdash\neg\diamondsuit\neg A$
sse para todo $w'$ com $Rww'$, $\mathbf{M},w'\Vdash A$. Novamente,
pela definição de $\mathbf{M},w\Vdash$, isso é o casso sse $\mathbf{M},w\Vdash\square A$.

2. Exercício
\end{proof}
%

\section{Verdade em um modelo}

Às vezes é de interesse investigar quais fórmulas são verdadeiras
em qualquer mundo em uma dado modelo. Introduziremos uma notação para
isto.\vspace{8pt}

\noindent{\fboxrule 0.1cm\fcolorbox{magenta}{white}{\begin{minipage}[t]{1\columnwidth - 2\fboxsep - 2\fboxrule}%
\begin{defn}
Uma fórmula $A$ é verdadeira em um modelo $\mathbf{M}=<W,R,V>$,
escrita $\mathbf{M}\Vdash A$, se e somente se $\mathbf{M},w\Vdash A$
para qualquer $w\in W$.
\end{defn}

%
\end{minipage}}}\vspace{8pt}

\begin{prop}
1. Se $\mathbf{M}\Vdash A$, então $\mathbf{M}\nVdash\neg A$, mas
não vice-versa

2. Se $\mathbf{M}\Vdash A\rightarrow B$, então $\mathbf{M}\Vdash A$
somente se $\mathbf{M}\Vdash B$, mas não vice-versa
\end{prop}

\begin{proof}
1. Se $\mathbf{M}\Vdash A$, então $A$ é verdadeiro em todos os mundos
possíveis em $W$ e, uma vez que $W\neq\emptyset$, não ser {[}o caso{]}
que $\mathbf{M}\Vdash A$, pois, caso contrário, $A$ teria de ser
verdadeiro e falso em algum mundo.

Por outro lado, se $\mathbf{M}\nVdash\neg A$, então $A$ é verdadeiro
em algum mundo $w\in W$. Não se segue que $\mathbf{M},w\Vdash A$,
\emph{para qualquer} $w\in W$. Por exemplo, no modelo da Figura \ref{fig:simples},
$\mathbf{M}\nVdash\neg p$ e também $\mathbf{M}\nVdash p$.

2. Assuma que $\mathbf{M}\Vdash A\rightarrow B$ e $\mathbf{M}\Vdash A$;
mostre que $\mathbf{M}\Vdash B$. Seja $w$ um mundo arbitrário. Então
$\mathbf{M},w\Vdash A\rightarrow B$ e $\mathbf{M},w\Vdash A$, assim
$\mathbf{M},w\Vdash B$. Uma vez que $w$ era arbitrário, $\mathbf{M}\Vdash B$.

Para mostrar que a inversa falha, precisamos encontrar um modelo $M$
tal que $\mathbf{M}\Vdash A$ somente se $\mathbf{M}\Vdash B$, mas
$\mathbf{M}\nVdash A\rightarrow B$. Considere novamente o modelo
da Figura \ref{fig:simples}: $\mathbf{M}\nVdash p$ e, portanto,
(vacuamente) $\mathbf{M}\Vdash p$ somente se $\mathbf{M}\Vdash q$.
Entretanto, $\mathbf{M}\nVdash p\rightarrow q$, pois $p$ é verdadeiro,
mas $q$ é falso em $w_{1}$.
\end{proof}
%

\section{Validade}

Fórmulas que são verdadeiras em todos os modelos, isto é, verdadeiras
em qualquer mundo em qualquer modelo, são particularmente interessantes.
Elas representam aquelas proposições modais que são verdadeiras independentemente
de como $\square$ e $\diamondsuit$ são interpretados, contanto que
a interpretação seja ``normal'' no sentido em que ela é gerada por
alguma relação de acessibilidade sobre mundos possíveis. Chamamos
tais fórmulas \emph{válidas}. Por exemplo, $\square(p\wedge q)\rightarrow\square p$
é válida. Algumas fórmulas que esperaríamos como sendo válida em base
da interpretação alética de $\square$ não são, entretanto, válidas.
Parte do interesse de modelos relacionais é que interpretações diferentes
de $\square$ e $\diamondsuit$ podem ser capturadas por diferentes
tipos de relações de acessibilidade. Isto sugere que deveríamos definir
validade não apenas relativa a todos \emph{os modelos}, mas também
relativa a todos os modelos \emph{de um certo tipo}. Será visto, por
exemplo, que {[}It will turn out, e. g., that{]} $\square p\rightarrow p$
é verdadeira em todos os modelos em que qualquer mundo é acessível
a partir de si mesmo, ou seja, quando $R$ é reflexiva. Definir validade
relativa a classes de modelos capacita-nos a formular isto de forma
sucinta: $\square p\rightarrow p$ é válida na classe de modelos reflexivos.\vspace{8pt}

\noindent{\fboxrule 0.1cm\fcolorbox{magenta}{white}{\begin{minipage}[t]{1\columnwidth - 2\fboxsep - 2\fboxrule}%
\begin{defn}
Uma fórmula $A$ \emph{é válida} em uma classe $\mathscr{C}$ de modelos,
se ela é verdadeira em qualquer modelo em $\mathscr{C}$ (ou seja,
verdadeira em qualquer mundo em qualquer modelo em $\mathscr{C}$).
Se $A$ é válida em $\mathscr{C}$, escrevemos $\mathscr{C}\models A$
e escrevemos $\models A$, se $A$ é válido na classe de \emph{todos}
os modelos.
\end{defn}

%
\end{minipage}}}\vspace{8pt}

\begin{prop}
Se $A$ é válida em $\mathscr{C}$, então ela é também válida em cada
classe $\mathscr{C}'\subseteq\mathscr{C}$.
\end{prop}

\begin{prop}
Se $A$ é válida, então $\square A$ é válida
\end{prop}

\begin{proof}
Assuma que $\models A$. Mostre que $\models\square A$. Seja $\mathbf{M}=<W,R,V>$
um modelo e $w\in W$. Se $Rww'$, então $\mathbf{M},w'\Vdash A$,
uma vez que $A$ é válida e, assim, $\mathbf{M},w'\Vdash\square A$.
Uma vez que $\mathbf{M}$ e $w$ são arbitrários, então $\models\square A$.
\end{proof}
%

\section{Instâncias tautológicas}

Uma fórmula modalmente livre {[}modal-free formula{]} se ela é verdadeira
sob qualquer atribuição de valor de verdade. Claramente qualquer tautologia
é verdadeira em qualquer mundo em qualquer modelo. Mas, para as fórmulas
que envolvem $\square$ e $\diamondsuit$, a noção de tautologia não
é definida. Por exemplo, $\square p\vee\neg\square p$ --- uma instância
do princípio do terceiro excluído --- é válido? A noção de \emph{instância
tautológica} ajuda: uma fórmula que é uma instância de substituição
de uma tautologia (não modal). Não é surpreendente, mas ainda requer
prova, o fato de que qualquer instância tautologia seja válida.

\vspace{8pt}

\noindent{\fboxrule 0.1cm\fcolorbox{magenta}{white}{\begin{minipage}[t]{1\columnwidth - 2\fboxsep - 2\fboxrule}%
\begin{defn}
Uma fórmula $B$ é uma instância tautológica se e somente se há uma
tautologia modalmente livre {[}modal-free tautology{]} $A$ com variáveis
proposicionais $p_{1},\ldots,p_{n}$ e fórmulas $D_{1},\ldots D_{n}$
tal que $B\equiv A[D_{1}/p_{1},\ldots,D_{n}/p_{n}]$.
\end{defn}

%
\end{minipage}}}

\vspace{8pt}

\begin{lem}
\label{lema14}Suponha que $A$ seja uma fórmula modalmente livre
cujas variáveis proposicionais são $p_{1},\ldots,p_{n}$ e sejam $D_{1},\ldots,D_{n}$
fórmulas modais. Então para qualquer atribuição $\mathcal{V}$, qualquer
modelo $\mathbf{M}=<W,R,V>$ e qualquer $w\in W$ tal que $\mathcal{V}(p_{i})=\mathrm{T}$
se e somente se $\mathbf{M},w\Vdash D_{i}$, temos que $v\models A$
se e somente se $\mathbf{M},w\Vdash A[D_{1}/p_{1},\ldots,D_{n}/p_{n}]$.
\end{lem}

\begin{proof}
Por indução sobre $A$. 1. $A\equiv\bot$: Tanto $\mathcal{V}\nvDash\bot$
como $\mathbf{M},w\models\bot$ \\2. $A\equiv p_{i}$:\\%
\begin{tabular}{ccll}
$\mathcal{V}\models p_{i}$ & $\Longleftrightarrow$ & $\mathcal{V}(p_{i})=\mathrm{T}$ & pela definição de $\mathcal{V}\models p_{i}$;\tabularnewline
 & $\Longleftrightarrow$ & $\mathbf{M},w\Vdash D_{i}$ & pela hipótese;\tabularnewline
 & $\Longleftrightarrow$ & $\mathbf{M},w\Vdash p_{i}[D_{1}/p_{1},\ldots,D_{n}/p_{n}]$ & pois $p_{i}[D_{1}/p_{1},\ldots,D_{n}/p_{n}]$.\tabularnewline
\end{tabular}\\3. $A\equiv\neg B$:\\%
\begin{tabular}{ccll}
$\mathcal{V}\models\neg B$ & $\Longleftrightarrow$ & $\mathcal{V}\nvDash\mathrm{B}$ & pela definição de $\mathcal{V}\models$;\tabularnewline
 & $\Longleftrightarrow$ & $\mathbf{M},w\nVdash B[D_{1}/p_{1},\ldots,D_{n}/p_{n}]$ & pela hipótese indutiva;\tabularnewline
 & $\Longleftrightarrow$ & $\mathbf{M},w\Vdash\neg B[D_{1}/p_{1},\ldots,D_{n}/p_{n}]$ & pela def. de $\mathcal{V}\models$.\tabularnewline
\end{tabular}\\4. $A\equiv(B\wedge C)$:\\%
\begin{tabular}{ccll}
$\mathcal{V}\models B\wedge C$ & $\Longleftrightarrow$ & $\mathcal{V}\models B$ e $\mathcal{V}\models C$ & pela definição de $\mathcal{V}\models$;\tabularnewline
 & $\Longleftrightarrow$ & $\mathbf{M},w\Vdash B[D_{1}/p_{1},\ldots,D_{n}/p_{n}]$ e  & \tabularnewline
 & $\Longleftrightarrow$ & $\mathbf{M},w\Vdash C[D_{1}/p_{1},\ldots,D_{n}/p_{n}]$ & pela hipótese indutiva;\tabularnewline
 & $\Longleftrightarrow$ & $\mathbf{M},w\Vdash(B\wedge C)[D_{1}/p_{1},\ldots,D_{n}/p_{n}]$ & pela definição de $\mathbf{M},w\Vdash$\tabularnewline
\end{tabular}\\5. $A\equiv(B\vee C)$: \\%
\begin{tabular}{ccll}
$\mathcal{V}\models B\vee C$ & $\Longleftrightarrow$ & $\mathcal{V}\models B$ ou $\mathcal{V}\models C$ & pela definição de $\mathcal{V}\models$;\tabularnewline
 & $\Longleftrightarrow$ & $\mathbf{M},w\Vdash B[D_{1}/p_{1},\ldots,D_{n}/p_{n}]$ ou & \tabularnewline
 & $\Longleftrightarrow$ & $\mathbf{M},w\Vdash C[D_{1}/p_{1},\ldots,D_{n}/p_{n}]$ & pela hipótese indutiva;\tabularnewline
 & $\Longleftrightarrow$ & $\mathbf{M},w\Vdash(B\vee C)[D_{1}/p_{1},\ldots,D_{n}/p_{n}]$ & pela definição de $\mathbf{M},w\Vdash$\tabularnewline
\end{tabular}\\6. $A\equiv(B\rightarrow C)$: \\%
\begin{tabular}{ccll}
$\mathcal{V}\models B\rightarrow C$ & $\Longleftrightarrow$ & $\mathcal{V}\nvDash B$ ou $\mathcal{V}\models C$ & pela definição de $\mathcal{V}\models$;\tabularnewline
 & $\Longleftrightarrow$ & $\mathbf{M},w\nVdash B[D_{1}/p_{1},\ldots,D_{n}/p_{n}]$ ou & \tabularnewline
 & $\Longleftrightarrow$ & $\mathbf{M},w\Vdash C[D_{1}/p_{1},\ldots,D_{n}/p_{n}]$ & pela hipótese indutiva;\tabularnewline
 & $\Longleftrightarrow$ & $\mathbf{M},w\Vdash(B\rightarrow C)[D_{1}/p_{1},\ldots,D_{n}/p_{n}]$ & pela definição de $\mathbf{M},w\Vdash$\tabularnewline
\end{tabular}
\end{proof}
%
\begin{prop}
Todas as instâncias tautológicas são válidas
\end{prop}

\begin{proof}
Vamos prova a contrapositiva. Suponha que $A$ é tal que $\mathbf{M},w\nVdash A[D_{1}/p_{1},\ldots,D_{n}/p_{n}]$
para algum modelo $\mathbf{M}$ e algum mundo $w$. Defina uma atribuição
$\mathcal{V}$ tal que $\mathcal{V}(p_{i})=\mathrm{T}$ se e somente
se $\mathbf{M},w\Vdash D_{i}$(e $\mathcal{V}$ atribui valores arbitrários
a $q\notin\{p_{1},\ldots,p_{n}\}$). Então pelo Lema \ref{lema14},
$\mathcal{V}\nvDash A$ e, assim, $A$ não é tautologia.
\end{proof}
%

\section{Esquemas e validade}

\vspace{8pt}

\noindent{\fboxrule 0.1cm\fcolorbox{magenta}{white}{\begin{minipage}[t]{1\columnwidth - 2\fboxsep - 2\fboxrule}%
\begin{defn}
Um esquema é um conjunto de fórmulas que inclui todas e somente {[}\emph{all
and only}{]} as instâncias de substituição de alguma fórmula modal
$C$, ou seja, $\{B:\exists D_{1},\ldots,\exists D_{n}(B=C[D_{1}/p_{1},\ldots,D_{n}/p_{n}])\}$
.

A fórmula $C$ é chamada a fórmula característica {[}\emph{characteristic
formula}{]} do esquema e ela é única até {[}up to{]} a renomeação
das variáveis proposicionais. Uma fórmula $A$ é uma instância de
um esquema, se ela é um membro do conjunto.
\end{defn}

%
\end{minipage}}}

\vspace{8pt}

É conveniente denotar um esquema por meio de expressão metalinguística
obtida por de meio da substituição dos componentes atômicos de $C$
por `$A$', `$B$',$\ldots$.Assim, por exemplo, os seguintes denotam
esquemas: `$A$', `$A\rightarrow\square A$', `$A\rightarrow(B\rightarrow A)$'.
Eles correspondem às fórmulas características $p$, $p\rightarrow\square p$,
$p\rightarrow(q\rightarrow p)$. O esquema `$A$' denota o conjunto
de \emph{todas} as fórmulas.

\vspace{8pt}

\noindent{\fboxrule 0.1cm\fcolorbox{magenta}{white}{\begin{minipage}[t]{1\columnwidth - 2\fboxsep - 2\fboxrule}%
\begin{defn}
Um esquema será \emph{verdadeiro }em um modelo se e somente se todas
as suas instâncias forem verdadeiras no modelo; e um esquema será
válido se e somente se ele for verdadeiro em qualquer modelo.
\end{defn}

%
\end{minipage}}}

\vspace{8pt}

\begin{prop}
O seguinte esquema K é válido:

\begin{equation}
\square(A\rightarrow B)\rightarrow(\square A\rightarrow\square B)\tag{K}
\end{equation}
\end{prop}

\begin{proof}
Precisamos mostrar que todas as instâncias do esquema são verdadeiras
em qualquer mundo em qualquer modelo. Assim, sejam $\mathbf{M}=<W,R,V>$
e $w\in W$ arbitrários. Para mostrar que um condicional é verdadeiro
em um mundo, assumimos que o antecedente é verdadeiro para mostrar
que o consequente é verdadeiro também, Neste caso, assuma que $\mathbf{M},w\Vdash\square(A\rightarrow B)$
e $\mathbf{M},w\Vdash\square A$. Precisamos mostrar que $\mathbf{M},w\Vdash\square B$.
Assim, seja $w'$ arbitrário tal que $Rww'$. Então, pela primeira
suposição, temos que $\mathbf{M},w'\Vdash A\rightarrow B$ e, pela
segunda suposição, temos que $\mathbf{M},w'\Vdash A$. Logo, segue-se
que $\mathbf{M},w'\Vdash B$. Uma vez que $w'$ era arbitrário, temos
que $\mathbf{M},w\Vdash\square B$.
\end{proof}
%
\begin{prop}
O seguinte esquema DUAL \emph{é válido\label{proposicao1.19}}

\begin{equation}
\diamondsuit A\leftrightarrow\neg\square\neg A\tag{DUAL}
\end{equation}
\end{prop}

\begin{proof}
Exercício
\end{proof}
%
\begin{prop}
Se $A$ e $A\rightarrow B$ são verdadeiras em um mundo, em um modelo,
então $B$ também é. Assim, as fórmulas válidas são fechadas sob modus
ponens.
\end{prop}

\begin{prop}
Uma fórmula $A$será válida sse todas as suas instâncias de substituição
forem também. Em outras palavras, um esquema é válido sse sua fórmula
característica também for. \label{proposicao1.21}
\end{prop}

\begin{proof}
A direção ``se'' é óbvia, uma vez que $A$é uma instância de substituição
de si mesma.

Para provar a direção ``somente se'', mostramos o seguinte: suponha
que $\mathbf{M}=<W,R,V>$ é um modelo modal e que $B\equiv A[D_{1}/p_{1},\ldots,D_{n}/p_{n}]$
é uma instância de substituição de $A$. Defina $\mathbf{M'}=<W,R,V'>$
por meio de $V'(p_{i})=\{w:\mathbf{M}\Vdash D_{i}w\}$. Então $\mathbf{M},w\Vdash B$
sse $\mathbf{M'},w\Vdash A$, para qualquer $w\in W$ (a prova será
deixada como exercício). Suponha agora que $A$ era válida, mas alguma
instância de substituição $B$ de A não era válida. Então, para algum
$\mathbf{M}=<W,R,V>$ e algum $w\in W$, $\mathbf{M},w\nVdash B$.
Mas, então, $\mathbf{M'},w\nVdash A$ pela reivindicação e $A$ não
é válida, uma contradição.
\end{proof}
%
Note, entretanto, que não é verdadeiro que um esquema seja verdadeiro
em um modelo sse sua fórmula característica também é. Obviamente,
a direção ``somente se'' vale: se qualquer instância de $A$é verdadeira
em $\mathbf{M}$, então a própria $A$ é verdadeira em $\mathbf{M}$.
Contudo, pode acontecer que $A$ seja verdadeira em $\mathbf{M}$,
mas alguma instância de $A$ seja falsa em algum mundo em $\mathbf{M}$.
Para um contraexemplo muito simples, considere $p$ em um modelo com
apenas um mundo $w$ e $V(p)=\{w\}$, de forma que $p$ é verdadeiro
em $w$. Mas $\bot$ é uma instância de $p$ e não é verdadeiro em
$w$.
\begin{center}
\begin{table}
\centering{}%
\begin{tabular}{|l|l|}
\hline 
Esquemas válidos & Esquemas inválidos\tabularnewline
\hline 
\hline 
$\square(A\rightarrow B)\rightarrow(\diamondsuit A\rightarrow\diamondsuit B)$ & $\square(A\vee B)\rightarrow(\square A\vee\square B)$\tabularnewline
$\diamondsuit(A\rightarrow B)\rightarrow(\square A\rightarrow\diamondsuit B)$ & $(\diamondsuit A\vee\diamondsuit B)\rightarrow\diamondsuit(A\wedge B)$\tabularnewline
$\square(A\wedge B)\leftrightarrow(\square A\wedge\square B)$ & $A\rightarrow\square A$\tabularnewline
$\square A\rightarrow\square(B\rightarrow A)$ & $\square\diamondsuit A\rightarrow B$\tabularnewline
$\neg\diamondsuit A\rightarrow\square(A\rightarrow B)$ & $\square\square A\rightarrow\square A$\tabularnewline
$\diamondsuit(A\vee B)\leftrightarrow(\diamondsuit A\vee\diamondsuit B)$ & $\square\diamondsuit A\rightarrow\diamondsuit\square A$\tabularnewline
\hline 
\end{tabular}\caption{Esquemas válidos e (ou?) inválidos\label{tabela1.1}}
\end{table}
\par\end{center}

\section{Acarretamento {[}\emph{entailment}{]}}

Com a definição de verdade em um mundo, podemos definir a relação
de acarretamento entre fórmulas. Uma fórmula $B$ acarreta $A$ sse
sempre que $B$ é verdadeira, $A$ é verdadeira também. Aqui, ``sempre
que'' significa ``qualquer que seja o modelo que consideramos''
assim como ``qualquer que seja o mundo neste modelo que consideramos''.

\vspace{8pt}

\noindent{\fboxrule 0.1cm\fcolorbox{magenta}{white}{\begin{minipage}[t]{1\columnwidth - 2\fboxsep - 2\fboxrule}%
\begin{defn}
Se $\varGamma$ é um conjunto de fórmulas e $A$ é uma fórmula, então
$\varGamma$ acareta $A$ --- em símbolos: $\varGamma\models A$---
se e somente se para qualquer modelo $\mathbf{M}=<W,R,V>$ e qualquer
mundo $w\in W$, se $\mathbf{M},w\Vdash B$ para qualquer $B\in\varGamma$,
então $\mathbf{M},w\Vdash A$. Se $\varGamma$ contém uma única fórmula
$B$, escrevemos $B\models A$.
\end{defn}

%
\end{minipage}}}

\vspace{8pt}

\begin{example}
Para mostrar que uma fórmula acarreta uma outra, temos de raciocionar
sobre todos os modelos, usando a definição de $\mathbf{M},w\Vdash$.
Por exemplo, para mostrar que $p\rightarrow\diamondsuit p\models\square\neg p\rightarrow\neg p$,
poderíamos argumentae como se segue: considere um modelo $\mathbf{M}=<W,R,V>$
e $w\in W$ e suponha que $\mathbf{M},w\Vdash p\rightarrow\diamondsuit p$.
Temos de mostrar que $\mathbf{M},w\Vdash\square\neg p\rightarrow\neg p$.
Suponha que isso não é o caso. Então $\mathbf{M},w\Vdash\square\neg p$
e $\mathbf{M},w\nVdash\neg p$. Uma vez que $\mathbf{M},w\nVdash\neg p$,
então $\mathbf{M},w\Vdash p$. Pela suposição, $\mathbf{M},w\Vdash p\rightarrow\diamondsuit p$,
assim $\mathbf{M},w\Vdash\diamondsuit p$. Pela definição de $\mathbf{M},w\Vdash\diamondsuit p$,
há um $w'$ com $Rww'$ tal que $\mathbf{M},w'\Vdash p$. Uma vez
que $\mathbf{M},w\Vdash\square\neg p$, temos que $\mathbf{M},w'\Vdash\neg p$,
uma contradição.

Para mostrar que uma fórmula $B$ não implica uma outra $A$, temos
de dar um contraexemplo, ou seja, um modelo $\mathbf{M}=<W,R,V>$
em que mostramos que em algum mundo $w\in W$, $\mathbf{M},w\Vdash B$,
mas $\mathbf{M},w\nVdash A$. Considere o modelo na Figura \ref{figura2}.
Temos que $\mathbf{M},w_{1}\Vdash\diamondsuit p$ e, assim, $\mathbf{M},w_{1}\Vdash p\rightarrow\diamondsuit p$.
Entretanto, uma vez que $\mathbf{M},w_{1}\Vdash\square p$, mas $\mathbf{M},w_{1}\nVdash p$,
temos que $\mathbf{M},w_{1}\nVdash\square p\rightarrow p$.

Frequentemente exemplos bastante simples são suficientes. O modelo
$\mathbf{M'}=\{W',R',V'\}$ com $W'=\{w\}$, $R'=\emptyset$ e $V(p)=\emptyset$
é também um contraexemplo: uma vez que $\mathbf{M'},w\nVdash p$,
então $\mathbf{M'},w\Vdash p\rightarrow\diamondsuit p$. Como nenhum
mundo é acessível a partir de $w$, temos que $\mathbf{M'},w\Vdash\square p$
e, assim, que $\mathbf{M'},w\nVdash\square p\rightarrow p$.
\end{example}

\begin{figure}
\begin{centering}
 \psscalebox{.7 .7} % Change this value to rescale the drawing. 
{
\begin{pspicture}(0,-3.6)(10.17,3.6) 
\pscircle[linecolor=black, linewidth=0.04, dimen=outer](1.2,2.4){1.2}
\pscircle[linecolor=black, linewidth=0.04, dimen=outer](8.4,2.4){1.2}
\pscircle[linecolor=black, linewidth=0.04, dimen=outer](4.8,-2.4){1.2} 
\rput[bl](0.8,2.4){$w_2$} 
\rput[bl](8.0,2.4){$w_3$} 
\rput[bl](4.4,-2.8){$w_1$}
\rput[bl](2.8,2.4){$p$} 
\rput[bl](10.0,2.4){$p$}
\rput[bl](6.4,-2.4){$\neg p$}
\psline[linecolor=black, linewidth=0.04, arrowsize=0.05291667cm 2.0,arrowlength=1.4,arrowinset=0.0]{->}(3.6,-1.2)(2.0,1.2)
\psline[linecolor=black, linewidth=0.04, arrowsize=0.05291667cm 2.0,arrowlength=1.4,arrowinset=0.0]{->}(6.0,-1.2)(8.0,1.2) 
\end{pspicture} 
}
\par\end{centering}
\caption{Contraexemplo para $p\rightarrow\diamondsuit p\protect\models\square p\rightarrow p$}

\label{figura2}

\end{figure}


\section{Problema}

\textbf{Problema 1.1} Considere o modelo da Figura \ref{fig:simples}.
Quais das seguintes afirmações valem?
\begin{enumerate}
\item $\mathbf{M},w_{1}\Vdash q$;
\item $\mathbf{M},w_{3}\Vdash\neg q$;
\item $\mathbf{M},w_{1}\Vdash p\vee q$;
\item $\mathbf{M},w_{1}\Vdash\square(p\vee q)$;
\item $\mathbf{M},w_{3}\Vdash\square q$;
\item $\mathbf{M},w_{3}\Vdash\square\bot$;
\item $\mathbf{M},w_{1}\Vdash\lozenge q$;
\item $\mathbf{M},w_{1}\Vdash\square q$
\item $\mathbf{M},w_{1}\Vdash\neg\square\square\neg q$
\end{enumerate}
\textbf{Problema 1.2} Complete a prova da Proposição \ref{proposicao1.7}

\noindent \textbf{Problema 1.3} Seja $\mathbf{M}=<W,R,V>$ um modelo
e suponha que $w_{1},w_{2}\in W$ são tais que:
\begin{enumerate}
\item $w_{1}\in V(p)$ se e somente se $w_{2}\in V(p)$; e
\item para todo $w\in W$, $Ew_{1}w$ se e somente se $Rw_{2}w$.
\end{enumerate}
Usando indução sobre fórmulas, mostre que para qualquer fórmula $A$:
$\mathbf{M},w_{1}\Vdash A$ se e somente se $\mathbf{M},w_{2}\Vdash A$.

\noindent \textbf{Problema 1.4} Seja $\mathbf{M}=<W,R,V>$. Mostre
que $\mathbf{M},w\Vdash\neg\diamondsuit A$ se e somente se $\mathbf{M},w\Vdash\square\neg A$.

\noindent \textbf{Problema 1.5} Considere o seguinte modelo $\mathbf{M}$
para a linguagem que contém $p_{1},p_{2},p_{3}$ como as únicas variáveis
proposicionais:
\begin{center}
 \psscalebox{.7 .7} % Change this value to rescale the drawing. 
{
\begin{pspicture}(0,-4.630786)(12.22,4.630786)
\pscircle[linecolor=black, linewidth=0.04, dimen=outer](2.24,1.6492139){1.46}
\pscircle[linecolor=black, linewidth=0.04, dimen=outer](10.1,1.709214){1.46} 
\pscircle[linecolor=black, linewidth=0.04, dimen=outer](6.1,-3.1707861){1.46} 
\rput[bl](1.92,1.5092139){$w_1$} 
\rput[bl](10.0,1.549214){$w_3$} 
\rput[bl](5.96,-3.350786){$w_2$}
\rput[bl](0.26,1.989214){$p_1$} 
\rput[bl](0.04,1.549214){$\neg p_2$}
\rput[bl](0.0,1.109214){$\neg p_3$} 
\rput[bl](11.92,2.009214){$p_1$}
\rput[bl](11.92,1.5092139){$p_2$}
\rput[bl](11.92,1.0092139){$p_3$}
\rput[bl](8.14,-2.790786){$p_1$}
\rput[bl](8.14,-3.290786){$p_2$} 
\rput[bl](7.96,-3.730786){$\neg p_3$}
\psline[linecolor=black, linewidth=0.04, arrowsize=0.05291667cm 2.0,arrowlength=1.4,arrowinset=0.0]{->}(7.2,-1.890786)(9.08,0.36921397) \psline[linecolor=black, linewidth=0.04, arrowsize=0.05291667cm 2.0,arrowlength=1.4,arrowinset=0.0]{->}(2.94,0.12921396)(4.7,-2.090786) \psline[linecolor=black, linewidth=0.04, arrowsize=0.05291667cm 2.0,arrowlength=1.4,arrowinset=0.0]{->}(3.8,1.789214)(8.4,1.789214) 
\rput{-43.384533}(0.06654787,7.865721){\psarc[linecolor=black, linewidth=0.04, dimen=outer, arrowsize=0.05291667cm 2.0,arrowlength=1.4,arrowinset=0.0]{<-}(9.92,3.8492138){0.68}{0.0}{270.0}} 
\end{pspicture} 
}
\par\end{center}

\noindent As seguinte fórmulas e esquemas são verdadeiras no modelo
$\mathbf{M}$, ou seja, verdadeiras em qualquer mundo em $\mathbf{M}$?
Explique.
\begin{enumerate}
\item $p\rightarrow\diamondsuit p$ (para $p$ atômica);
\item $A\rightarrow\diamondsuit A$ (para $A$ arbitrária);
\item $\square p\rightarrow p$ (para $p$ atômica);
\item $\neg p\rightarrow\lozenge\square p$ (para $p$ atômica);
\item $\diamondsuit\square A$ (para $A$arbitrária);
\item $\diamondsuit\square p$ (para $p$ atômica).
\end{enumerate}
\textbf{Problema 1.7} Mostre que $A\rightarrow\square A$ é valida
na classe $\mathscr{C}$ de modelos $\mathbf{M}=<W,R,V>$, em que
$W=\{w\}$. Similarmente mostre que $B\rightarrow\square A$ e $\diamondsuit A\rightarrow B$
são válidas na classe de modelos $\mathbf{M}=<W,R,V>$, em que $R=\emptyset$.

\noindent \textbf{Problema 1.8} Prove a Proposição \ref{proposicao1.19}

\noindent \textbf{Proposição 1.9} Prove a reivindicação na parte ``somente
se'' da prova da Proposição \ref{proposicao1.21} (dica: use indução
sobre $A$).

\noindent \textbf{Proposição 1.10} Mostre que nenhuma das seguintes
fórmulas são válidas:
\begin{enumerate}
\item[D:]  $\square p\rightarrow\diamondsuit p$;
\item[T:] $\square p\rightarrow p$;
\item[B:] $p\rightarrow\square\diamondsuit p$;
\item[4:] $\square p\rightarrow\square\square p$;
\item[5:] $\diamondsuit p\rightarrow\square\diamondsuit p$.
\end{enumerate}
\textbf{Problema 1.11} Prove que os esquemas na primeira coluna da
tabela \ref{tabela1.1} são válidos e os das segunda coluna são inválidos.

\noindent \textbf{Problema 1.12} Decida se os seguintes esquemas são
válidos ou inválidos:
\begin{enumerate}
\item $(\diamondsuit A\rightarrow\square B)\rightarrow(\square A\rightarrow\square B)$;
\item $\diamondsuit(A\rightarrow B)\vee\square(B\rightarrow A)$.
\end{enumerate}
\textbf{Problema 1.13} Para cada um dos seguintes esquemas, encontre
um modelo $\mathbf{M}$ tal que qualquer instância da fórmula é verdadeira
em $\mathbf{M}$:
\begin{enumerate}
\item $p\rightarrow\diamondsuit\diamondsuit p$
\item $\diamondsuit p\rightarrow\square p$
\end{enumerate}
\textbf{Problema 1.14} Mostre que $\square(A\wedge B)\models\square A$.

\noindent \textbf{Problema 1.15} Mostre que $\square(p\rightarrow q)\nvDash p\rightarrow\square q$
e $p\rightarrow\square q\nvDash\square(p\rightarrow q)$.

\chapter{Definabilidade de estrutura {[}Frame definability{]}}

\section{Introdução}

Uma questão que interessa aos lógicos modais é a conexão entre a relação
de acessibilidade e a verdade de certas fórmulas nos modelos com esta
relação de acessibilidade. Por exemplo, suponha que a relação de acessibilidade
é reflexiva, ou seja, para qualquer $w\in W$, Rww. Em outros palavras,
qualquer mundo é acessível a partir de si mesmo. Isto significa que
quando $\square A$ é verdadeiro em um mundo w, o próprio w está entre
os mundos acessíveis em que A deve ser, portanto, verdadeiro. Assim,
se a relação de acessibilidade R de $\mathbf{M}$ é reflexiva, então
quaisquer que sejam o mundo w e a fórmula A que tomamos, $\square A\rightarrow A$
será verdadeiro no modelo (em outra palavras, o esquema $\square p\rightarrow p$
e todas as instâncias de substituição dele são verdadeiras em $\mathbf{M}$).

A inversa, entretanto, é falsa. Por exemplo, não é o caso que se $\square p\rightarrow p$
é verdadeira em $\mathbf{M}$, então $R$é reflexiva. Pois podemos
encontrar facilmente um modelo $\mathbf{M}$ não-reflexivo em que
$\square p\rightarrow p$ é verdadeira em todos os mundos: tome o
modelo com um único mudo $w$, que não é acessível a partir de si
mesmo, mas com $w\in V(p)$. Selecionando o valor de verdade de $p$
adequadamente, podemos fazer $\square A\rightarrow A$ verdadeira
em um modelo que não é reflexivo.

A solução é remover a atribuição de variável $V$ da equação. Se exigirmos
que $\square p\rightarrow p$ é verdadeira em todos os mundos em $W$,
independentemente de quais mundos estão em $V(p)$, então é necessário
que $R$ seja reflexiva. Pois, em qualquer modelo não-reflexivo, haverá
pelo menos um mundo $w$ tal que não é o caso que $Rww$. Se estabelecermos
$V(p)=W\backslash\{w\}$, então $p$ será verdadeira em todos os mundos,
exceto em $w$ e, assim, será verdadeira em todos os mundos acessíveis
a partir de $w$ (uma vez que é garantido que $w$ não é acessível
a partir de $w$ e $w$ é o único mundo em que $p$ é falsa). Por
outro lado, $p$ é falsa em $w$ e, assim, $\square p\rightarrow p$
é falsa em $w$.

Isto sugere que deveríamos introduzir uma notação para estruturas
de modelo sem uma valoração: chamamo-las \emph{frames}. Um \emph{frame}
$\mathcal{F}$ é simplesmente um par $<W,R>$ que consiste em um conjunto
de mundos com uma relação de acessibilidade. Qualquer modelo $<W,R,V>$
é, então, como dizemos, baseado no \emph{frame} $<W,R>$. Inversamente,
um \emph{frame} determina a classe de modelos baseados nele; e uma
classe de \emph{frames} determina a classe de modelos que são baseados
em qualquer \emph{frame} na classe. E podemos definir $\mathcal{F}\models A$,
a noção de uma fórmula ser \emph{válida} em um \emph{frame} como:
$\mathbf{M}\Vdash A$ para todo $\mathbf{M}$ baseado em $\mathcal{F}$.

Com esta notação, podemos estabelecer relações de correspondência
entre fórmulas e classes de \emph{frames}: por exemplo, $\mathcal{F}\models\square p\rightarrow p$
se e somente se $\mathcal{F}$ é reflexivo.

\section{Propriedades de relações de acessibilidade}

Algumas fórmulas modais são resultantes de características de propriedades
simples, e até mesmo comuns, da relação de acessibilidade. Por um
lado, isto significa que qualquer modelo que tem uma dada propriedade
faz a fórmula correspondente (e todas as instâncias de substituição
dela) verdadeira. Começamos com cinco exemplos clássicos de tipos
de relações de acessibilidade e fórmulas cuja verdade eles garantem.
\begin{thm}
\label{Teorema2-1}Seja $M=<W,R,V>$ um modelo. Se $R$ tem a propriedade
à esquerda da tabela \ref{tabela2-1}, qualquer instância da fórmula
à direita é verdadeira em $\mathbf{M}$.
\end{thm}

\begin{proof}
Aqui é o caso para B: para mostrar que o esquema é verdadeiro em um
modelo, precisamos mostrar que todas as instâncias do esquema são
verdadeiras em todos os mundos no modelo. Assim, seja $A\rightarrow\diamondsuit\square A$
uma dada instância de B e seja $w\in W$ um mundo arbitrário. Suponha
que o antecedente $A$ é verdadeiro em $w$, a fim de mostrar que
$\square\diamondsuit A$ é verdadeira em $w$. Assim, precisamos mostrar
que $\diamondsuit A$ é verdadeira em todos os mundos $w'$ acessíveis
a partir de $w$. Ora, para qualquer $w'$ tal que $Rww'$, temos
também, usando a hipótese da simetria, que $Rw'w$ (veja a Figura
\ref{figura2-1}). Uma vez que $\mathbf{M},w\Vdash A$, temos que
$\mathbf{M},w'\Vdash\diamondsuit A$. Uma vez que $w'$ era um mundo
arbitrário tal que $Rww'$, temos que $\mathbf{M},w\Vdash\square\diamondsuit A$. 

Deixamos os outros casos como exercício.
\end{proof}
%
\begin{table}
\begin{centering}
\begin{tabular}{|l|l|}
\hline 
\emph{Se R é ...} & então ... é verdadeira em $\mathbf{M}$\tabularnewline
\hline 
\hline 
serial: $\forall u\exists vRuv$ & $\square p\rightarrow\diamondsuit p$\hfill{}(D)\tabularnewline
\hline 
reflexiva: $\forall wRww$ & $\square p\rightarrow p$\hfill{}(T)\tabularnewline
\hline 
simetria: $\forall u\forall v(Ruv\rightarrow Rvu)$ & $p\rightarrow\square\diamondsuit p$\hfill{}(B)\tabularnewline
\hline 
transitiva: $\forall u\forall v\forall w(Ruv\wedge Rvw\rightarrow Ruw)$ & $\square p\rightarrow\square\square p$\hfill{}(4)\tabularnewline
\hline 
euclidiana: $\forall w\forall u\forall v(Rwu\wedge Rwv\rightarrow Ruv)$ & $\diamondsuit p\rightarrow\square\diamondsuit p$\hfill{}(5)\tabularnewline
\hline 
\end{tabular}
\par\end{centering}
\caption{Cinco fatos de correspondência\label{tabela2-1}}

\end{table}

\begin{figure}
\begin{centering}
\psscalebox{.7 .7} % Change this value to rescale the drawing. 
{ 
\begin{pspicture}(0,-1.18)(5.18,1.18)
\pscircle[linecolor=black, linewidth=0.04, dimen=outer](0.63,0.53){0.63}
\rput[bl](0.46,0.44){$w$} \rput[bl](4.42,0.46){$w'$} 
\psline[linecolor=black, linewidth=0.04, arrowsize=0.05291667cm 2.0,arrowlength=1.4,arrowinset=0.0]{->}(1.38,1.16)(3.82,1.14) 
\psline[linecolor=black, linewidth=0.04, arrowsize=0.05291667cm 2.0,arrowlength=1.4,arrowinset=0.0]{->}(3.7,0.02)(1.4,0.0) 
\rput[bl](0.04,-0.68){$\Vdash A$} 
\rput[bl](0.04,-1.18){$\Vdash\square\diamondsuit A$}
\rput[bl](4.16,-0.62){$\Vdash\diamondsuit A$}
\pscircle[linecolor=black, linewidth=0.04, dimen=outer](4.55,0.55){0.63} 
\end{pspicture} 
} 
\par\end{centering}
\caption{O argumento a partir da simetria\label{figura2-1}}

\end{figure}

Note que as implicações inversas do Teorema \ref{Teorema2-1} não
valem: não é verdade que se um modelo verifica um esquema, então a
relação de acessibilidade deste modelo tem a propriedade correspondente.
No caso de T e modelos reflexivos, é fácil dar um contraexemplo de
um modelo no qual o próprio T falha: Sejam $W=\{w\}$ e $V(p)=\emptyset$.
Então $R$ não é reflexivo, mas $\mathbf{M},w\Vdash\square p$ e $\mathbf{M},w\nVdash p$.
Mas, aqui, temos justamente uma única instância de T que falha em
$\mathbf{M}$, outras instâncias, por exemplo, $\square\neg p\rightarrow\neg p$,
são verdadeiras. É mais difícil dar exemplos em que qualquer instância
de substituição de T é verdadeira em $\mathbf{M}$ e $\mathbf{M}$
não é reflexiva. Mas há também tais modelos:
\begin{prop}
Seja $\mathbf{M}=<W,R,V>$ um modelo tal que $W=\{u,v\}$, em que
os mundos $u$ e $v$ estão relacionados pela R: ou seja, tanto $Ruv$
como $Rvu$. Suponha que para todo $p$: $u\in V(p)\Leftrightarrow v\in V(p)$.
Então:

1. Para todo $A$: $\mathbf{M},u\Vdash A$ se e somente se $\mathbf{M},v\Vdash A$
(use indução sobre A).

2. Qualquer instância de T é verdadeira em $\mathbf{M}$.

\noindent Uma vez que $\mathbf{M}$ não é reflexiva (de fato, é irreflexiva),
a inversa do Teorema \ref{Teorema2-1} falha no caso de T (argumentos
similares podem ser dados para alguns --- embora não todos --- dos
outros esquemas mencionados no Teorema \ref{Teorema2-1}.
\end{prop}

Embora nosso foco será nas cinco fórmulas clássicas D, T, B, 4 e 5,
registramos na tabela \ref{tabela2-2} mais algumas propriedades de
relações de acessibilidade. A relação de acessibilidade $R$ é parcialmente
funcional, se a partir de qualquer mundo no máximo um mundo é acessível.
Se é o caso que de qualquer mundo exatamente um mundo é acessível,
chamamo-la funcional. (Assim as relações funcionais são precisamente
aquelas que são tanto seriais como parcialmente funcionais). Elas
são chamadas funcionais, porque a relação de acessibilidade opera
como uma função (parcial). Uma relação é fracamente densa se sempre
que $Ruv$, existe um $w$ ``entre'' $u$ e $v$.

\begin{table}
\begin{centering}
\begin{tabular}{|>{\raggedright}p{5cm}|l|}
\hline 
\emph{Se R é ...} & então ... é verdadeira em $\mathbf{M}$\tabularnewline
\hline 
\hline 
parcialmente funcional: $\forall w\forall u\forall v(Rwu\wedge Rwv\rightarrow u=v)$ & $\diamondsuit p\rightarrow\square p$\tabularnewline
\hline 
funcional: $\forall w\exists u\forall v(Rwu\leftrightarrow u=v)$ & $\diamondsuit p\leftrightarrow\square p$\tabularnewline
\hline 
fracamente densa: $\forall u\forall v(Ruv\rightarrow\exists w(Ruw\wedge Rwv)$ & $\square\square p\rightarrow\square p$\tabularnewline
\hline 
fracamente conectada: $\forall w\forall u\forall v(Rwu\wedge Rwv\rightarrow Ruv\vee u=v\vee Rvu)$ & $\square((p\wedge\square p)\rightarrow q)\vee\square((q\wedge\square q)\rightarrow p)$\tabularnewline
\hline 
fracamente direcionada: $\forall w\forall u\forall v(Rwu\wedge Rwv\rightarrow\exists t(Rut\wedge Rvt))$ & $\diamondsuit\square p\rightarrow\square\diamondsuit p$\tabularnewline
\hline 
\end{tabular}
\par\end{centering}
\caption{Mais cinco fatos de correspondência\label{tabela2-2}}
\end{table}

\end{document}
